Business applications have gained widespread use, despite their complexity and the difficulty in accurately projecting their performance. Businesses use applications for tasks including reimbursing employees for travel expenses, ordering notebooks and other office supplies, allocating office and cubicle space, and other routine trivia, as well as for more complex tasks such as the bookkeeping and organizational procedures by which on-line auction houses organize auctions, banks handle checks, insurance companies decide what sort of policy to issue, railroad companies track trains' locations and contents, etc. Business applications need to be flexible in ways that more typical, linear computer programs do not. As an example, a business application which automatically processes employee travel vouchers must be capable of evaluating a plurality of contingent conditions (e.g., employee status, employee travel allocations, expenditure ceilings, approval requirements, etc.) and of processing or routing requests based on the evaluation of those conditions. Further, business applications necessarily rely heavily on human action, such as when human judgment is essential to a resolution of an atypical transaction. Well-designed business systems have escape commands in which privileged users (e.g., managers) can “violate” the general requirements and invariants of the system as necessary in order to deal with reality.
For preliminary diagnostic purposes, with the intent of eliminating “bugs” during software design, it is desirable to create models of the software which demonstrate where problems may occur in the finished product. Due to the nature of business applications, the behavior of fully-developed business applications is somewhat unpredictable and tends to be difficult to model. Nonetheless, given the fact that business applications are expensive to develop and use, and generally even more expensive to retrofit when bugs have been detected after the applications are in user it is prudent to evaluate the applications in the early design to locate detectable defects by modeling the behavior of the application. The desire for detecting defects is realistically offset by the practicalities of modeling. Clearly not all behaviors can be checked unless the entire application is executed, which would be a prohibitively lengthy and intensive modeling process.
Model checking is a preferred method for formally evaluating the behavior of a business application. In model checking, such as is detailed in the publications entitled Model Checking by E. M. Clarke, et al, MIT Press, (Cambridge, Mass., 1999) and Model Checking Large Software Specifications by N. Carriero, et al, IEEE Transactions on Software Engineering, pages 498-519 (July 1998), a system is described as a finite-state model and a desired property of the system is expressed as a logical formula. Having the finite-state model and the logical formula, it can be determined whether the system has the desired property. While computationally complex applications cannot realistically be fully modeled, due to exponential expansion of the possible decision paths, many useful cases can be analyzed.
Ordered Boolean Decision Diagrams (OBDDs) have been a very successful approach to model checking, providing a compact canonical notation for Boolean expressions, in which all the basic operations are efficiently computable. The model must be phrased as Boolean formulas, for example, with the state s as a vector of Boolean variables, formulas St(s) describe the possible start states, and Trans(s,t) describing when the system can take a transition from s to t. The multi-step behavior of the system can then be computed from these (e.g., the set of reachable states is computed from the transitive closure:                {r|∃s .St (sTrans(s,t)}.        
Temporal logic formulas (e.g., Computation Tree Logic or CTL), can also be expressed as OBDDs. Checking whether or not the model satisfies the formula then becomes a matter of calculation. In many useful cases, OBDD calculations can be done quickly. This approach has verified properties of system with astounding numbers of states, currently up to 10120 for well-designed systems and properties. Model checking with such systems, however, takes a significant amount of human work in setting up the problem. Therefore, while model checking has theoretical potential in many arenas, it has primary usefulness in the areas of protocol checking and circuit checking, wherein the models are inherently small and of regular structure. Model checking has had limited applicability in checking routine software.
With regard to software checking, model checking has been used not for verification but for so-called falsifying of properties, wherein selected bugs in the system can be targeted and found. For example, one may see if a protocol can deadlock or a memory management chip can lose a page. Clearly, these are important properties to identify and correct. Checking a handful of well-chosen properties can catch many errors, and can increase confidence that remaining errors are scattered and more benign. Some properties, however, may simply be too hard to check.
Additional shortcomings of model checking include the fact that the models must be kept as small as possible, due to the fact that even a bit or two in the wrong place can greatly increase computation time. By reducing model size, however, one necessarily sacrifices some degree of certainty that the model is adequate for its checking purposes. It must also be recognized that the real system (i.e., the business application being checked) is must larger than the model and that verification via the model which concludes that an application does not produce errors in its execution of four consecutive processes cannot predict that the application will not lock upon execution of the fifth process.
Therefore, it is desirable, and is an object of the present invention, to provide a method and apparatus for checking a business application for detectable defects in the early application design using model checking.
It is another object of the invention to provide a method and apparatus for applying model checking for verification of selected aspects of business application software.
Yet another object of the invention is to provide a method which gives a total, programmatic description of classes and activities of a business application as well as a partial, logical description of specifications therein.